1: | x - 0 | → x | |
2: | s(x) - s(y) | → x - y | |
3: | p(s(x)) | → x | |
4: | f(s(x),y) | → f(p(s(x) - y),p(y - s(x))) | |
5: | f(x,s(y)) | → f(p(x - s(y)),p(s(y) - x)) | |
6: | s(x) -# s(y) | → x -# y | |
7: | F(s(x),y) | → F(p(s(x) - y),p(y - s(x))) | |
8: | F(s(x),y) | → P(s(x) - y) | |
9: | F(s(x),y) | → s(x) -# y | |
10: | F(s(x),y) | → P(y - s(x)) | |
11: | F(s(x),y) | → y -# s(x) | |
12: | F(x,s(y)) | → F(p(x - s(y)),p(s(y) - x)) | |
13: | F(x,s(y)) | → P(x - s(y)) | |
14: | F(x,s(y)) | → x -# s(y) | |
15: | F(x,s(y)) | → P(s(y) - x) | |
16: | F(x,s(y)) | → s(y) -# x | |